COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	HERE IS A SAMPLE DIALOGUE WITH A PROGRAM GENERATOR-VERIFIER
C00005 00003	EXAMPLE 2.  Here is the generation-verification of the iterative
C00006 ENDMK
C⊗;
HERE IS A SAMPLE DIALOGUE WITH A PROGRAM GENERATOR-VERIFIER
WHICH USES HOARE'S RULES EXPRESSED IN VCGEN.

We wish to write a procedure named FACT of two arguments,one of
which is a parameter named a, and the other is to take be assigned
r value. Name this second argument,r. The parameter,a, can take on
values ≥0; the output  is to be such that r=a!.

→   USE V8

P(proc q(x,v);A}R   1

→   LET P,R,q,x,v BE a≥0,r=a!,FACT,r,a

a≥0{proc FACT(r,a);A} r=a!     2

→   TRY

a≥0{FACT(r,a)}r=a! ||- a≥0{A} r=a!   3 (1,2)

→   USE V5 3(2)

a≥0{A; IF Q THEN B ELSE C}r=a!   4

→   TRY

a≥0∧Q{A;B}r=a!   a≥0∧¬Q{A;C}r=a!  5 (1 ,2)

→   LET Q,A BE a=0,null

a≥0∧a=0{B}r=a!   a≥0∧a≠0{C}r=a!   6(1,2)

→   TRIVIAL a≥0∧a=0⊃a=0,a≥0∧a≠0⊃a>0

→   SIMP 6

a=0{B}r=a!    a>0{C}r=a!  7(1,2)

→   SHOW 1

a≥0{proc FACT(r,a);IF a=0 THEN B ELSE C}r=a!

→   GO 7(1)

→   LET B BE r←1

a=0{r←1}r=a! 8

→TRY V1,V3

a=0{null}1=a! 9
a=0⊃1=a! 10

→   TRIVIAL a=0⊃1=a!

7(1) ESTABLISHED,
a=0{r←1}r=a!  a>0{C}r=a! 11(1,2)
a>0{C}r=a!

→   LET C BE FACT(r,a-1);r←r*a

a>0{FACT(r,a-1);r←r*a}r=a!  12

→   USE V1

a>0{FACT(r,a-1)}r*a=a!  13

→   TRY V7

U(x;v){FACT(x;v)}W(x;v)  a>0{null}U(r,a-1)∧∀r(W(r,a-1)⊃r*a=a!)  14

→   LET U(x,v), W(x,v) BE x≥0,x=v!

x≥0{FACT(x,v)}x=v! a>0{null}r≥0∧∀r(r=a-1!)⊃r*a=a!) 15

→   BACK 14

→   LET U(x,v), W(x,v) BE v≥0,x=v!

v≥0{FACT(x,v)}x=v! a>0{null}a-1≥0∧∀r(r=a-1!⊃r*a=a!) 16

→   USE V3,3(1)

a>0⊃a-1≥0∧∀r(r=a-1!⊃r*a=a!) 17

→   TRIVIAL 17[1]

→   PROVABLE 17[2]

7(2) ESTABLISHED,
7 ESTABLISHED,
1 ESTABLISHED,
 
PROGRAM IS:

{proc FACT(r,a);IF a=0 THEN r←1 ELSE FACT(r,a-1);r←r*a}

ASSUMPTIONS ARE:
   TRIVIAL
a≥0∧a=0 ⊃ a=0
a≥0∧a=0 ⊃ a>0

   PROVABLE
r=a-1! ⊃ r*a=a!

EXAMPLE 2.  Here is the generation-verification of the iterative
form of the factorial function.

→   USE V8

P{proc q(x,v);A}R 1

→   LET P,R,q,x,v BE a≥0,r=a!,FACT,r,a

a≥0{proc FACT(r,a)A} r=a!   2

→   TRY

a≥0{FACT(r,a)}r=a! ||- a≥0{A} r=a!  3(1,2)

→   USE V4 3(2)

a≥0{A;R WHILE S DO B}r=a!  4

→   TRY

a≥0{A}R R∧S{B}R R∧¬S⊃r=a!  5(1,2,3)

→   LET S BE a≠0

a≥0{A}R  R∧a≠0{B}R  R∧¬a≠0⊃r=a! 6(1,2,3)

→   TRIVIAL a≡¬a≠0

→   SIMP 6

a≥0{A}R R∧a≠0{B}R  R∧a=0⊃r=a!  7(1,2,3)

→   LET A BE x←a;r←1;